Issue478b.agda:9,9-12
Set₁ !=< T
when checking that the expression Set has type T
